$\forall$$k$:Knd, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$a$:Knd fp$\rightarrow$ Top, $f$:(Id$\times$Top) List, $x$:Id, $t$:Type, $v$:$t$.
\\[0ex]${\it ds}$ $\parallel$ $x$ : $t$
\\[0ex]$\Rightarrow$ (with declarations ds:${\it ds}$da:${\it da}$$k$(v) sends $f$ s v on link $l$ $\Vert\!+$ $x$ : $t$ initially $x$ = $v$)